\documentclass{article}
\usepackage{amsmath,tkz-linknodes}
\usepackage{tikz}

%\usepackage[graphics,tightpage,active]{preview}
%\PreviewEnvironment{NodesList}
\newlength{\imagewidth}
\newlength{\imagescale}

\input{common}

\begin{document}
\thispagestyle{empty}
\begin{NodesList}[margin=3cm]
\begin{align*}
  \alpha [\phi \wedge \psi] & = \alpha [\phi] \sqcap \alpha [\psi] \AddNode \\
% \intertext{\hfil \ldots by the inductive step\ldots \hfil}
  & = (\alpha [\phi] \sqcap \alpha) \sqcap (\alpha [\psi] \sqcap \alpha) \AddNode \\ %& \tmop{by \alphanduction}
  & = ((\alpha [\phi] \sqcap \alpha) \sqcap \alpha [\psi]) \sqcap \alpha \AddNode \\
  & = (\alpha [\phi] \sqcap (\alpha \sqcap \alpha [\psi])) \sqcap
  \alpha \AddNode \\
& = (\alpha [\phi] \sqcap (\alpha[\psi] \sqcap \alpha )) \sqcap \alpha
\AddNode \\
& = ((\alpha [\phi] \sqcap \alpha[\psi]) \sqcap \alpha ) \sqcap \alpha
\AddNode \\
& = (\alpha [\phi] \sqcap \alpha[\psi]) \sqcap (\alpha  \sqcap \alpha)
\AddNode \\
  & = (\alpha [\phi] \sqcap \alpha [\psi]) \sqcap \alpha \AddNode \\
  & = \alpha [\phi \wedge \psi] \sqcap \alpha \AddNode
\end{align*}
 
 \tikzset{LabelStyle/.append style = {\myside},
            ArrowStyle/.append style = {draw=\mydraw}}
\LinkNodes {Inductive step}%
\LinkNodes{Associativity}
\LinkNodes{Associativity}
\LinkNodes{Commutativity}
\LinkNodes{Associativity}
\LinkNodes{Associativity}
\LinkNodes{Since $\alpha \sqcap \alpha = \alpha$}
\LinkNodes{By definition}
   \end{NodesList}
\end{document}
